Factor out goto model processing and default options #2049
Conversation
karkhaz
requested review from
kroening,
peterschrammel,
smowton and
tautschnig
as code owners
There was a problem hiding this comment.
This refactoring is great, and my requests-for-more-work are all only possible because you started this line of work. Sorry that it means there is even more work to do... @peterschrammel @kroening could you comment on whether some of that work is also useful to simplify/reduce redundancy with other *_parse_optionst instances?
src/cbmc/cbmc_parse_options.cpp
Outdated
| @@ -111,6 +130,8 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) | |||
| if(cmdline.isset("paths")) | |||
| options.set_option("paths", true); | |||
|
|
|||
| cbmc_parse_optionst::set_default_options(options); | |||
|
|
|||
There was a problem hiding this comment.
Nit pick: may I suggest to move this up by three lines to be the very first step before doing if(cmdline.isset...?
src/cbmc/cbmc_parse_options.cpp
Outdated
| options.set_option("simplify-if", true); | ||
|
|
||
| // Default false | ||
| options.set_option("stop-on-fail", false); |
There was a problem hiding this comment.
Could you please add unwinding-assertions, partial-loops, slice-formula in here and refactor their current command-line/options code to use if(cmdline.isset...)?
src/cbmc/cbmc_parse_options.cpp
Outdated
| const optionst &options) | ||
| goto_modelt &goto_model, | ||
| const optionst &options, | ||
| const cmdlinet &cmdline, |
There was a problem hiding this comment.
Your change highlights one existing poor design: this function should not be using cmdline anymore, anything it cares about ought to have been placed in options. Could you please clean this up as well?
src/cbmc/cbmc_parse_options.cpp
Outdated
| const cmdlinet &cmdline, | ||
| messaget &log, | ||
| ui_message_handlert &ui_message_handler, | ||
| message_handlert &mh) |
There was a problem hiding this comment.
mh and ui_message_handler will actually be the same in the context of cbmc_parse_optionst, and both of which you'd get by doing log.get_message_handler(). What you wouldn't be able to get, though, is ui_message_handler.get_ui() so maybe pass that in addition to just a messaget?
src/cbmc/cbmc_parse_options.cpp
Outdated
| const optionst &options, | ||
| const cmdlinet &cmdline, | ||
| messaget &log, | ||
| message_handlert &mh) |
There was a problem hiding this comment.
As above: just pass log, and obtain mh via log.get_message_handler().
karkhaz
force-pushed
the
kk-factor-goto-model-processing
branch
2 times, most recently
from
20594cf to
0859693
Compare
|
Just pushed some changes. Please could you confirm that the hunk at cbmc_parse_options.cpp:224 captures the right intention? I think this is a bit more explicit than before, even, since the code before would silently ignore At the severe risk of creating more work for myself...there are queries to I think eventually it might be desirable to avoid passing |
karkhaz
force-pushed
the
kk-factor-goto-model-processing
branch
from
0859693 to
85e8d63
Compare
There was previously no public interface to check whether an option had been set in an optionst object; this meant that clients were instead using the isset() method of cmdlinet. This change allows us to set the options from the cmdlinet near the beginning of the front-end, and not refer to the cmdlinet afterward.
karkhaz
force-pushed
the
kk-factor-goto-model-processing
branch
from
85e8d63 to
9af0a1c
Compare
CBMC parse options that have default values are all set in a single
place---a static method that may also be called from any client that
needs to emulate CBMC's default options (e.g. unit tests). Previous to
this commit, there were a lot of
if(cmdline.isset("no-foo"))
options.set_option("foo", false);
else
options.set_option("foo", true);
This commit removes all the else cases.
karkhaz
force-pushed
the
kk-factor-goto-model-processing
branch
from
9af0a1c to
b7b9ad9
Compare
|
All checks passed. I implemented your suggestion of changing |
src/cbmc/cbmc_parse_options.cpp
Outdated
| options.set_option("bounds-check", true); | ||
|
|
||
| if(cmdline.isset("pointer-check")) | ||
| options.set_option("pointer-check", true); |
There was a problem hiding this comment.
"pointer-check" and "bounds-check" are actually covered by PARSE_OPTIONS_GOTO_CHECK below so those two can be skipped here.
src/cbmc/cbmc_parse_options.cpp
Outdated
| cmdline.isset("unwinding-assertions")); | ||
| error() << "--cover and --unwinding-assertions " | ||
| << "must not be given together" << eom; | ||
| exit(CPROVER_EXIT_USAGE_ERROR); |
There was a problem hiding this comment.
It's probably a good idea to communicate this to users explicitly.
| nondet_static(goto_model); | ||
| } | ||
|
|
||
| if(cmdline.isset("string-abstraction")) | ||
| if(options.get_bool_option("string-abstraction")) |
There was a problem hiding this comment.
I don't think this option is getting set above?
| @@ -777,21 +806,21 @@ bool cbmc_parse_optionst::process_goto_program( | |||
| // add loop ids | |||
| goto_model.goto_functions.compute_loop_numbers(); | |||
|
|
|||
| if(cmdline.isset("drop-unused-functions")) | |||
| if(options.get_bool_option("drop-unused-functions")) | |||
There was a problem hiding this comment.
This needs to be checked as well above, I think.
src/cbmc/cbmc_parse_options.cpp
Outdated
| { | ||
| error() << "--reachability-slice and --reachability-slice-fb " | ||
| << "must not be given together" << eom; | ||
| log.error() << "--reachability-slice and --reachability-slice-fb " |
There was a problem hiding this comment.
May I suggest moving this options-collision checking up with the cmdline parsing? Errors should be flagged as early as possible.
|
sigh thanks for pointing these out. My strategy was to set the option for each command-line that was causing a test somewhere to fail. So all of the ones you pointed out don't have sufficient test coverage that it made a difference that I missed setting their option 😞 I now feel that this is fragile and prone to drift apart in the future---in both directions: where somebody misses setting an option, or where an option is accidentally set twice like in I'll sort these out tomorrow, need to sleep now, but maybe I'll think of a more robust way of doing this (or I'd appreciate any suggestions). I've often fantasied about writing a new |
Is #1521 of some help in this regard? Not that it specifies one single solution, but at least there is discussion - please do chime in! Other than that: yes, better test coverage is needed, or really just a record of current test coverage. There has been some work on that, but AFAIK that got put on the backlog. |
karkhaz
force-pushed
the
kk-factor-goto-model-processing
branch
2 times, most recently
from
8aa1ea1 to
3e4a77e
Compare
|
Comments are addressed, all checks are passing. I'll wait until I at least have a skeleton implementation before chiming in, I want to see if my ideas are practical. (One other thing that I wanted to have is a command line interface that could dump itself as {ba,z}sh completion files, man pages, etc...there's already a script that does this, but it would be nice to do it programatically rather than parsing cmdline text, since then we could also pass type information to zsh completion and so on) |
|
This looks great -- one question, to what degree can this be factored with JBMC? |
|
@smowton my feeling is that it might end up becoming a mess of front-end specific checks if we used the same static method? E.g. JBMC needs a I haven't actually tried it, but it looks like there would have to be e.g. a |
|
Fair enough, leave it then |
src/cbmc/cbmc_parse_options.cpp
Outdated
| options.set_option("simplify", true); | ||
| options.set_option("simplify-if", true); | ||
|
|
||
| // Default false |
There was a problem hiding this comment.
I am wondering: should this part actually be omitted completely? It does make a difference if the (new) is_set is used, but for get_bool_option setting them to false is as good as not setting them.
Edit: many other options also default to false, but are not being set here. I'm always after consistency...
CBMC's methods for getting a goto-model from a source file, and processing that goto-model to be ready for bounded model checking, are now static so that they can be called from clients that wish to set up a goto-model the same way that CBMC does.
karkhaz
force-pushed
the
kk-factor-goto-model-processing
branch
from
3e4a77e to
014d151
Compare
|
@tautschnig I removed the default-false options. |
ad62682 Merge pull request diffblue#2071 from thk123/refactor/split-string-unit-tests fc8ba88 Revert to aborting precondition for function inputs 3e2ab6f Merge pull request diffblue#2080 from diffblue/java-bytecode-dependency 6ff1eec cbmc: remove dependency on java_bytecode 0bff19b Merge pull request diffblue#2049 from karkhaz/kk-factor-goto-model-processing 79e3b25 Merge pull request diffblue#2084 from tautschnig/has_subtype-test cd45b0b Test has_subtype on recursive data types 85ac315 Merge pull request diffblue#2082 from thomasspriggs/default_dstring_hash 28c2e8b Merge pull request diffblue#2065 from tautschnig/be-constructor afa6023 Merge pull request diffblue#2061 from tautschnig/simplify-extractbits 014d151 Factor out getting & processing goto-model 06b3adc Merge pull request diffblue#2077 from peterschrammel/stable-tmp-var-names 0b3170d Stabilize clinit wrapper function type parameters 3cd8bf4 Temporary vars tests for goto-diff 9f0626c Prefix temporary var names with function id ca678aa More permissive regression tests regarding tmp var suffixes 47951ca Merge pull request diffblue#2079 from romainbrenguier/bugfix/has-subtype-recursion dd73b1a Specify default hash function of `dstringt` to STL. fe8e589 Avoid infinite recursion in has_subtype 00b9bf6 Merge pull request diffblue#2051 from svorenova/generics_tg2717 cd4bfc3 Merge pull request diffblue#2078 from romainbrenguier/bool-literal-in-while-loop 67ea889 Use bool literal in while loop d229ad9 Merge pull request diffblue#2056 from diffblue/fix-regression-cbmc-memcpy1 506faf0 Refactor a function for base existence 617d388 Utility functions for generic types c07e6ca Update generic specialization map when replacing pointers ed26d0a Merge pull request diffblue#2058 from peterschrammel/stable-disjuncts b663734 Simplify extractbits(concatenation(...)) b091560 Typing and refactoring of simplify_extractbits 49ad1bd Merge pull request diffblue#974 from tautschnig/fix-assert-encoding 16e9599 Merge pull request diffblue#2063 from tautschnig/has-subtype 950f58b Merge pull request diffblue#2060 from tautschnig/opt-local-map 4222a94 Regression tests for unstable instanceof and virtual method disjuncts b44589e Make disjuncts in instanceof removal independent of class loading 3afff86 Make disjuncts in virtual method removal independent of class loading a385d9b Allowed split_string to be used on whitespace if not also trying to strip fe4a642 Merge pull request diffblue#2062 from tautschnig/no-has-deref 145f474 Adding tests for empty string edge cases 07009d4 Refactored test to run all combinations 252c24c Migrate old string utils unit tests e87edbf Removing wrong elements from the make file b165c52 make test work on 32-bit Linux b804570 Merge pull request diffblue#2048 from JohnDumbell/improvement/adding_null_object_id 61f14d8 Merge pull request diffblue#1962 from owen-jones-diffblue/owen-jones-diffblue/simplify-replace-java-nondet fdee7e8 Merge pull request diffblue#2059 from tautschnig/generalise-test 4625cc5 Extend global has_subexpr to take a predicate as has_subtype does e9ebd59 has_subtype(type, pred, ns) to search for contained type matching pred 1f1f67f Merge pull request diffblue#1889 from hannes-steffenhagen-diffblue/develop-feature_generate_function_bodies 048c188 Add unit test for java_replace_nondet 0fe48c9 Make remove_java_nondet work before remove_returns bcc4dc4 Use byte_extract_exprt constructor a1814a3 Get rid of thin (and duplicate) has_dereference wrapper 4122a28 Test to demonstrate assert bug on alpine d44bfd3 Also simplify assert structure found on alpine linux c5cde18 Do not generate redundant if statements in assert expansions 4fb0603 Make is_skip publicly available and use constant argument 5832ffd Negative numbers should also pass the test 3c23b28 Consistently disable simplify_exprt::local_replace_map da63652 Merge pull request diffblue#2054 from romainbrenguier/bugfix/clear-equations d77f6a2 Merge pull request diffblue#1831 from NathanJPhillips/feature/class-annotations 60c8296 Clear string_refinement equations (not dependencies) 314ed53 Correcting the value of ID_null_object 751a882 Factor out default CBMC options to static method 6f24009 Can now test for an option being set in optionst 9a8d937 Add to_annotated_type and enable type_checked_cast for annotated_typet ca77b4e Add test for added annotations b06a27d Introduce abstract qualifierst base class e6fb3bf Pretty printing of java_class_typet e22b95b Fix spurious virtual function related keywords 3ac6d17 Add type_dynamic_cast and friends for java_class_typet ce1f4d2 Add annotations to java_class_typet, its methods and fields f84753d Merge pull request diffblue#2042 from hannes-steffenhagen-diffblue/add_deprecate_macro 7a38669 Merge pull request diffblue#2017 from NathanJPhillips/feature/overlay-classes 75a4aec Revert "the deprecation will need to wait until codebase is clean" 67735b5 Disable deprecation warnings by default 0764f77 Merge pull request diffblue#2036 from romainbrenguier/id_array_list 690b606 Merge pull request diffblue#2039 from peterschrammel/fix-duplicate-msg-json-ui bba17d9 the deprecation will need to wait until codebase is clean 822c757 Regression test for redundant JSON message output de0644d Only force end of previous message if there actually is one. 5a637bf Merge pull request diffblue#2037 from hannes-steffenhagen-diffblue/add_deprecate_macro bff456a Merge pull request diffblue#2040 from tautschnig/remove-swp 87ebe90 Remove vim temp file 228c019 Fix duplicate message output in json-ui 0a2c43e Add DEPRECATED to functions documented as \deprecated 47f4b35 interval_sparse_arrayt constructor from array-list 026c4ca Declare an array_list_exprt class 50a2696 Define ID_array_list 513b67a Merge pull request diffblue#2038 from romainbrenguier/bugfix/assign-at-malloc-site c207106 Test with array of strings 60183a3 Assign string at malloc site 116fffd Add DEPRECATED macro to mark deprecated functions and variables 7952f2c Add option to generate function body to goto-instrument 3d4183a Add ability to overlay classes with new definitions of existing methods dbc2f71 Improve code and error message in infer_opaque_type_fields 7c0ea4d Tidied up java_class_loader_limitt git-subtree-dir: cbmc git-subtree-split: ad62682
This PR introduces a static method for setting CBCM's default options, and makes two of
cbmc_parse_optiont's methods static (for getting and processing a goto-model). This is so that clients that wish to emulate CBMC's functionality can do so by calling into these static methods, rather than duplicating code that is currently scattered through the file.